\begin{tabbing}
ESMachineAxiom($E$;$T$;$V$;$M$;${\it loc}$;${\it knd}$;${\it val}$;
\\[0ex]${\it when}$;${\it after}$;
\\[0ex]${\it sndr}$;${\it Trans}$;${\it Send}$;${\it Choose}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\forall$$e$:$E$.\+\+
\\[0ex]($\lambda$$x$.${\it after}$($x$,$e$)) $=$ ${\it Trans}$(${\it loc}$($e$),${\it knd}$($e$),${\it val}$($e$),$\lambda$$x$.${\it when}$($x$,$e$)) $\in$ $x$:Id$\rightarrow$$T$(${\it loc}$($e$),$x$))
\-\\[0ex]\& (\=$\forall$$e$:$E$.\+
\\[0ex]islocal(${\it knd}$($e$))
\\[0ex]$\Rightarrow$ \=isl(${\it Choose}$(${\it loc}$($e$),act(${\it knd}$($e$)),$\lambda$$x$.${\it when}$($x$,$e$)))\+
\\[0ex]\& \=${\it val}$($e$)\+
\\[0ex]$=$
\\[0ex]outl(${\it Choose}$(${\it loc}$($e$),act(${\it knd}$($e$)),$\lambda$$x$.${\it when}$($x$,$e$)))
\\[0ex]$\in$ $V$(${\it loc}$($e$),act(${\it knd}$($e$))))
\-\-\-\\[0ex]\& (\=$\forall$$e$:$E$.\+
\\[0ex]isrcv(${\it knd}$($e$))
\\[0ex]$\Rightarrow$ ($\langle$lnk(${\it knd}$($e$))$,\,$tag(${\it knd}$($e$))$,\,$(${\it val}$($e$))$\rangle$ $\in$ \=${\it Send}$\+
\\[0ex](${\it loc}$(${\it sndr}$($e$))
\\[0ex],${\it knd}$(${\it sndr}$($e$))
\\[0ex],${\it val}$(${\it sndr}$($e$))
\\[0ex],$\lambda$$x$.${\it when}$($x$,${\it sndr}$($e$))) $\in$ Msg($M$)))
\-\-\-
\end{tabbing}